…hange)

Splits the existing TcCtt resolution logic into three named local helpers — strat_tvar_via_tvtc, strat_abs_via_decl, strat_infer_by_carrier — corresponding to catalog modes #5, #6, and #1/#2 in doc/typeclasses-inference.md.

Behavior is identical: same dispatch order, same failures, same pickup of [Tvar a]/[Tconstr p] cases, same parking of univar carriers. The refactor exists so Phase 3 can drop a By-args strategy in without disturbing the existing logic.

Five related fixes that unblock multi-param TC inference:

1. UniEnv.tparams now derefs each tc_arg through Unify.close so the
   stored ax_tparams of a lemma carry resolved Tvars, not the stale
   Tunivars left over from typing-time opentvi calls. Without this,
   reusing a lemma whose tparams had constraints over earlier tparams
   left the constraint args as unbound Tunivars.

2. Tvar.subst_tc was a no-op — now it actually walks tc_args and
   substitutes through them. pf_check_tvi relied on this to
   instantiate constraints before infer.

3. TC class declarations (axioms + ops) thread ~tw_uni when calling
   Tuni.subst, matching the lemma path.

4. Unifier's `TcCtt` no-deps branch now parks on arg_deps when the
   carrier is concrete but its TC arg univars are still pending,
   instead of failing outright. Prevents premature failure when a TC
   op is type-checked before its arguments.

5. eq_tc compares TC arg types only, not their tcwitness components.
   The witnesses are determined by the (carrier, args) and may
   legitimately differ in shape (TCIUni vs TCIAbstract) while picking
   out the same TC at the structural level — comparing them
   prevented Mode #5 from matching a candidate whose type args
   matched but whose witnesses were typing-time stale.

Plus: `Tunivar↔Tunivar` union now merges the two sources' byunivar
entries onto the new representative so parked TC problems still fire
when the canonical univar is later bound.

Effects: tc/parametric.ec and tc/multi-param.ec now pass.